Termination w.r.t. Q proof of TRS/higher-order/AotoYam003.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(app(if, true), x), y) → x
app(app(app(if, false), x), y) → y
app(app(app(until, p), f), x) → app(app(app(if, app(p, x)), x), app(app(app(until, p), f), app(f, x)))

Q is empty.

↳ QTRS

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(app(if, true), x), y) → x
app(app(app(if, false), x), y) → y
app(app(app(until, p), f), x) → app(app(app(if, app(p, x)), x), app(app(app(until, p), f), app(f, x)))

Q is empty.